
; Copyright (c) 2015 Microsoft Corporation

;; Proofs for some identities found by Ramanujan


;; Problem 1
(simplify (^ (- (^ 2. (/ 1. 3.)) 1.) (/ 1. 3.)))

(simplify (+ (^ (/ 1. 9.) (/ 1. 3.))
             (* (- 1.) (^ (/ 2. 9.) (/ 1. 3.)))
             (^ (/ 4. 9.) (/ 1. 3.))))

(set-option :pp.decimal true)
(simplify (^ (- (^ 2. (/ 1. 3.)) 1.) (/ 1. 3.)))
          
(simplify (= (^ (- (^ 2. (/ 1. 3.)) 1.) (/ 1. 3.))
             (+ (^ (/ 1. 9.) (/ 1. 3.))
                (* (- 1.) (^ (/ 2. 9.) (/ 1. 3.)))
                (^ (/ 4. 9.) (/ 1. 3.)))))

;; Problem 2
(set-option :pp.decimal false)
(simplify (^ (- (* 7. (^ 20. (/ 1. 3.)))
                19.)
             (/ 1. 6.)))

(simplify (- (^ (/ 5. 3.) (/ 1. 3.))
             (^ (/ 2. 3.) (/ 1. 3.))))
(set-option :pp.decimal true)
(simplify (- (^ (/ 5. 3.) (/ 1. 3.))
             (^ (/ 2. 3.) (/ 1. 3.))))

(simplify (= (^ (- (* 7. (^ 20. (/ 1. 3.)))
                   19.)
                (/ 1. 6.))
             (- (^ (/ 5. 3.) (/ 1. 3.))
                (^ (/ 2. 3.) (/ 1. 3.)))))

;; Problem 3
(set-option :pp.decimal false)
(simplify (^ (/ (+ 3. (* 2.      (^ 5. (/ 1. 4.))))
                (+ 3. (* (- 2.)  (^ 5. (/ 1. 4.)))))
             (/ 1. 4.)))

(simplify (/ (+ (^ 5. (/ 1. 4.)) 1.)
             (- (^ 5. (/ 1. 4.)) 1.)))
(set-option :pp.decimal true)
(simplify (/ (+ (^ 5. (/ 1. 4.)) 1.)
             (- (^ 5. (/ 1. 4.)) 1.)))

(simplify (= (^ (/ (+ 3. (* 2.      (^ 5. (/ 1. 4.))))
                   (+ 3. (* (- 2.)  (^ 5. (/ 1. 4.)))))
                (/ 1. 4.))
             (/ (+ (^ 5. (/ 1. 4.)) 1.)
                (- (^ 5. (/ 1. 4.)) 1.))))

;; Problem 4
(set-option :pp.decimal false)
(simplify (^ (+ (^ (/ 1. 5.) (/ 1. 5.)) (^ (/ 4. 5.) (/ 1. 5.))) (/ 1. 2.)))
(simplify (^ (+ 1. (^ 2. (/ 1. 5.)) (^ 8. (/ 1. 5.))) (/ 1. 5.)))
(simplify (= (^ (+ (^ (/ 1. 5.) (/ 1. 5.)) (^ (/ 4. 5.) (/ 1. 5.))) (/ 1. 2.))
             (^ (+ 1. (^ 2. (/ 1. 5.)) (^ 8. (/ 1. 5.))) (/ 1. 5.))))

;; False equality
(simplify (= (^ (- (* 7. (^ 20. (/ 1. 3.))) 19.) (/ 1. 6.))
             (- (^ (/ 5. 3.) (/ 1. 4.)) (^ (/ 2. 3.) (/ 1. 3.)))))

